es:ES, e1, e2:E. e1  e2   (last(es-hist{i:l}(es;e1;e2)) ~ es-info(es;e2)) 

latex

Definitions	b, t  T, Top, x:A. B(x), loc(e), Id, E, S  T, [e, e'], P  Q, es-hist{i:l}(es;e1;e2), ES, e  e' , False, A, P  Q, (e <loc e'), P & Q, P  Q, Prop, null(as)
Lemmas	es-interval-last, assert of null, assert wf, null wf3, not functionality wrt iff, es-interval-nil, es-interval wf, es-locl wf, es-le-not-locl, es-le-loc, es-loc-pred, es-le wf, event system wf, last-map, es-interval wf2, top wf, es-E wf, Id wf, es-loc wf